The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
↳2 CdtProblem
↳3 CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication)
↳4 CdtProblem
↳5 CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID))
↳6 CdtProblem
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
↳8 CdtProblem
↳9 CdtKnowledgeProof (⇔)
↳10 CdtProblem
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
↳12 CdtProblem
↳13 CdtKnowledgeProof (⇔)
↳14 CdtProblem
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
↳16 CdtProblem
↳17 CdtKnowledgeProof (⇔)
↳18 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

test(x_0, y) → True
test(x_0, y) → False
append(l1_2, l2_1) → match_0(l1_2, l2_1, l1_2)
match_0(l1_2, l2_1, Nil) → l2_1
match_0(l1_2, l2_1, Cons(x, l)) → Cons(x, append(l, l2_1))
part(a_4, l_3) → match_1(a_4, l_3, l_3)
match_1(a_4, l_3, Nil) → Pair(Nil, Nil)
match_1(a_4, l_3, Cons(x, l')) → match_2(x, l', a_4, l_3, part(a_4, l'))
match_2(x, l', a_4, l_3, Pair(l1, l2)) → match_3(l1, l2, x, l', a_4, l_3, test(a_4, x))
match_3(l1, l2, x, l', a_4, l_3, False) → Pair(Cons(x, l1), l2)
match_3(l1, l2, x, l', a_4, l_3, True) → Pair(l1, Cons(x, l2))
quick(l_5) → match_4(l_5, l_5)
match_4(l_5, Nil) → Nil
match_4(l_5, Cons(a, l')) → match_5(a, l', l_5, part(a, l'))
match_5(a, l', l_5, Pair(l1, l2)) → append(quick(l1), Cons(a, quick(l2)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(MATCH_2(z2, z3, z0, z1, part(z0, z3)), PART(z0, z3))
MATCH_2(z0, z1, z2, z3, Pair(z4, z5)) → c8(MATCH_3(z4, z5, z0, z1, z2, z3, test(z2, z0)), TEST(z2, z0))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(MATCH_2(z2, z3, z0, z1, part(z0, z3)), PART(z0, z3))
MATCH_2(z0, z1, z2, z3, Pair(z4, z5)) → c8(MATCH_3(z4, z5, z0, z1, z2, z3, test(z2, z0)), TEST(z2, z0))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
K tuples:none
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, MATCH_1, MATCH_2, QUICK, MATCH_4, MATCH_5

Compound Symbols:

c2, c4, c5, c7, c8, c11, c13, c14

(3) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 1 of 8 dangling nodes:

MATCH_2(z0, z1, z2, z3, Pair(z4, z5)) → c8(MATCH_3(z4, z5, z0, z1, z2, z3, test(z2, z0)), TEST(z2, z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(MATCH_2(z2, z3, z0, z1, part(z0, z3)), PART(z0, z3))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(MATCH_2(z2, z3, z0, z1, part(z0, z3)), PART(z0, z3))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
K tuples:none
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, MATCH_1, QUICK, MATCH_4, MATCH_5

Compound Symbols:

c2, c4, c5, c7, c11, c13, c14

(5) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
K tuples:none
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, QUICK, MATCH_4, MATCH_5, MATCH_1

Compound Symbols:

c2, c4, c5, c11, c13, c14, c7

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
We considered the (Usable) Rules:

quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
part(z0, z1) → match_1(z0, z1, z1)
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
test(z0, z1) → True
test(z0, z1) → False
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
And the Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(APPEND(x1, x2)) = 0   
POL(Cons(x1, x2)) = [4] + x2   
POL(False) = [1]   
POL(MATCH_0(x1, x2, x3)) = 0   
POL(MATCH_1(x1, x2, x3)) = [3]   
POL(MATCH_4(x1, x2)) = x2   
POL(MATCH_5(x1, x2, x3, x4)) = x4   
POL(Nil) = 0   
POL(PART(x1, x2)) = [3]   
POL(Pair(x1, x2)) = x1 + x2   
POL(QUICK(x1)) = x1   
POL(True) = [1]   
POL(append(x1, x2)) = [2]   
POL(c11(x1)) = x1   
POL(c13(x1, x2)) = x1 + x2   
POL(c14(x1, x2, x3)) = x1 + x2 + x3   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(c7(x1)) = x1   
POL(match_0(x1, x2, x3)) = [3] + [3]x1 + [3]x2 + [4]x3   
POL(match_1(x1, x2, x3)) = x3   
POL(match_2(x1, x2, x3, x4, x5)) = [4] + x5   
POL(match_3(x1, x2, x3, x4, x5, x6, x7)) = [3] + x1 + x2 + x7   
POL(match_4(x1, x2)) = [3] + [2]x1 + [3]x2   
POL(match_5(x1, x2, x3, x4)) = [2] + [3]x1 + [3]x2 + [4]x3   
POL(part(x1, x2)) = x2   
POL(quick(x1)) = 0   
POL(test(x1, x2)) = [1]   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
K tuples:

MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, QUICK, MATCH_4, MATCH_5, MATCH_1

Compound Symbols:

c2, c4, c5, c11, c13, c14, c7

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
K tuples:

MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
QUICK(z0) → c11(MATCH_4(z0, z0))
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, QUICK, MATCH_4, MATCH_5, MATCH_1

Compound Symbols:

c2, c4, c5, c11, c13, c14, c7

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
We considered the (Usable) Rules:

quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
part(z0, z1) → match_1(z0, z1, z1)
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
test(z0, z1) → True
test(z0, z1) → False
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
And the Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(APPEND(x1, x2)) = 0   
POL(Cons(x1, x2)) = [2] + x2   
POL(False) = 0   
POL(MATCH_0(x1, x2, x3)) = 0   
POL(MATCH_1(x1, x2, x3)) = x3   
POL(MATCH_4(x1, x2)) = x22   
POL(MATCH_5(x1, x2, x3, x4)) = [1] + x42   
POL(Nil) = 0   
POL(PART(x1, x2)) = x2   
POL(Pair(x1, x2)) = x1 + x2   
POL(QUICK(x1)) = x12   
POL(True) = 0   
POL(append(x1, x2)) = 0   
POL(c11(x1)) = x1   
POL(c13(x1, x2)) = x1 + x2   
POL(c14(x1, x2, x3)) = x1 + x2 + x3   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(c7(x1)) = x1   
POL(match_0(x1, x2, x3)) = 0   
POL(match_1(x1, x2, x3)) = x3   
POL(match_2(x1, x2, x3, x4, x5)) = [2] + x5   
POL(match_3(x1, x2, x3, x4, x5, x6, x7)) = [2] + x1 + x2   
POL(match_4(x1, x2)) = 0   
POL(match_5(x1, x2, x3, x4)) = 0   
POL(part(x1, x2)) = x2   
POL(quick(x1)) = 0   
POL(test(x1, x2)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
K tuples:

MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, QUICK, MATCH_4, MATCH_5, MATCH_1

Compound Symbols:

c2, c4, c5, c11, c13, c14, c7

(13) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
K tuples:

MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, QUICK, MATCH_4, MATCH_5, MATCH_1

Compound Symbols:

c2, c4, c5, c11, c13, c14, c7

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
We considered the (Usable) Rules:

quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
part(z0, z1) → match_1(z0, z1, z1)
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
test(z0, z1) → True
test(z0, z1) → False
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
And the Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(APPEND(x1, x2)) = x1   
POL(Cons(x1, x2)) = [1] + x2   
POL(False) = 0   
POL(MATCH_0(x1, x2, x3)) = x3   
POL(MATCH_1(x1, x2, x3)) = 0   
POL(MATCH_4(x1, x2)) = x22   
POL(MATCH_5(x1, x2, x3, x4)) = [2]x4 + x42   
POL(Nil) = 0   
POL(PART(x1, x2)) = 0   
POL(Pair(x1, x2)) = x1 + x2   
POL(QUICK(x1)) = x12   
POL(True) = 0   
POL(append(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c13(x1, x2)) = x1 + x2   
POL(c14(x1, x2, x3)) = x1 + x2 + x3   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(c7(x1)) = x1   
POL(match_0(x1, x2, x3)) = x2 + x3   
POL(match_1(x1, x2, x3)) = x3   
POL(match_2(x1, x2, x3, x4, x5)) = [1] + x5   
POL(match_3(x1, x2, x3, x4, x5, x6, x7)) = [1] + x1 + x2   
POL(match_4(x1, x2)) = [2]x2   
POL(match_5(x1, x2, x3, x4)) = [1] + [2]x4   
POL(part(x1, x2)) = x2   
POL(quick(x1)) = [2]x1   
POL(test(x1, x2)) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

test(z0, z1) → True
test(z0, z1) → False
append(z0, z1) → match_0(z0, z1, z0)
match_0(z0, z1, Nil) → z1
match_0(z0, z1, Cons(z2, z3)) → Cons(z2, append(z3, z1))
part(z0, z1) → match_1(z0, z1, z1)
match_1(z0, z1, Nil) → Pair(Nil, Nil)
match_1(z0, z1, Cons(z2, z3)) → match_2(z2, z3, z0, z1, part(z0, z3))
match_2(z0, z1, z2, z3, Pair(z4, z5)) → match_3(z4, z5, z0, z1, z2, z3, test(z2, z0))
match_3(z0, z1, z2, z3, z4, z5, False) → Pair(Cons(z2, z0), z1)
match_3(z0, z1, z2, z3, z4, z5, True) → Pair(z0, Cons(z2, z1))
quick(z0) → match_4(z0, z0)
match_4(z0, Nil) → Nil
match_4(z0, Cons(z1, z2)) → match_5(z1, z2, z0, part(z1, z2))
match_5(z0, z1, z2, Pair(z3, z4)) → append(quick(z3), Cons(z0, quick(z4)))
Tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
S tuples:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
K tuples:

MATCH_4(z0, Cons(z1, z2)) → c13(MATCH_5(z1, z2, z0, part(z1, z2)), PART(z1, z2))
MATCH_5(z0, z1, z2, Pair(z3, z4)) → c14(APPEND(quick(z3), Cons(z0, quick(z4))), QUICK(z3), QUICK(z4))
QUICK(z0) → c11(MATCH_4(z0, z0))
MATCH_1(z0, z1, Cons(z2, z3)) → c7(PART(z0, z3))
PART(z0, z1) → c5(MATCH_1(z0, z1, z1))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
Defined Rule Symbols:

test, append, match_0, part, match_1, match_2, match_3, quick, match_4, match_5

Defined Pair Symbols:

APPEND, MATCH_0, PART, QUICK, MATCH_4, MATCH_5, MATCH_1

Compound Symbols:

c2, c4, c5, c11, c13, c14, c7

(17) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

APPEND(z0, z1) → c2(MATCH_0(z0, z1, z0))
MATCH_0(z0, z1, Cons(z2, z3)) → c4(APPEND(z3, z1))
Now S is empty

(18) BOUNDS(O(1), O(1))